x:T. P(x) == case xm({y:T| P(y)} ) of inl(z) => z | inr(w) => "???" 

latex

---

clarification:

choicef(xm; T; x.P(x)) == case xm({y:T| P(y)} ) of inl(z) => z | inr(w) => "???" 

latex

FDL editor aliases

choicef